1. Field
The present invention relates to modeling and testing digital designs of state machines, and more specifically, to systems, methods and computer products for the identification of dependent state variables to aid in logic design and verification.
2. Description of Related Art
A system such as an electrical circuit including state holding elements may be modeled using state equations and state variables that describe the behavior and state of the system. A complete set of state variables for a system, coupled with logic that defines the transitions between states, typically contains enough information about the system's history to enable computation of the system's future behavior. Simplifying the model to reduce the number of state variables, or simplifying the logic that defines state transitions, lessens the computational cost of analyzing the model, for example, to verify that it conforms to a given specification.
The synthesis and verification of state variable models often requires a great deal of computational resources. Numerous conventional frameworks for synthesis and verification of modets rely upon the paradigm of merging equivalent (or opposite-functionality) gates to enhance some optimality criteria. In synthesis, merging equivalent gates generally implies a smaller, lower power circuit. In verification, merging equivalent gates often has a variety of benefits such as speeding up falsification and proof algorithms.
Most high performance frameworks for deriving gates which may be merged use an assume-then-prove framework to speculatively reduce the size of the collective merging proof obligation by substitution of fanout references to merge candidates. While useful to simplify the proof obligation, one weakness is that if any of the merge candidates are determined to be invalid (e.g., they may functionally differ), the entire verification problem must be cast anew by “refinement”—that is, by forming a new speculatively-merged problem that discards the invalid merge candidates, and iterating this process until all merge candidates are be proven to be equivalent. This restart cost of discarding all verification results upon a refinement tends to be very expensive.
What is needed is a more efficient way of state variable model synthesis and verification.